switch between fifo+ send S1(j;i;e)
switch between fifo+ srequest Req1(i;e)
switch between fifo+ sacknowledge Ack1(j;i;e) and
switch between fifo+ send S2(j;i;e) request Req2(i;e) acknowledge Ack2(j;i;e)
== (i, j:C, x, y:E.
== (S2(j;i;x)
== ( S1(j;i;y)
== ( ((x c y
== ( (( (req:{e:E| S2(j;i;e)} 
== ( (( (ack:{e:E| Ack2(j;i;e)} . (Req2(j;req) & x c req & req c ack & ack c y)))
== ( & (y c x
== ( & ( (req:{e:E| S1(j;i;e)} 
== ( & ( (ack:{e:E| Ack1(j;i;e)} . (Req1(j;req) & y c req & req c ack & ack c x)))))
== & (i, j:C.
== & ((e, e':{e:E| Ack1(j;i;e)} . (e' c e)  (e < e'))
== & (& (e, e':{e:E| Ack2(j;i;e)} . (e' c e)  (e < e')))
== & (i, j:C.
== & ((e, e':{e:E| S1(j;i;e) & Req1(j;e)} . (e' c e)  (e < e'))
== & (& (e, e':{e:E| S2(j;i;e) & Req2(j;e)} . (e' c e)  (e < e')))
== & (i, j:C.
== & ((e, e':{e:E| S1(j;i;e) & Req1(j;e)} .
== & (((e < e')  (a:{e:E| Ack1(j;i;e)} . ((e < a) & (a < e'))))
== & (& (e, e':{e:E| S2(j;i;e) & Req2(j;e)} .
== & (& ((e < e')  (a:{e:E| Ack2(j;i;e)} . ((e < a) & (a < e'))))) 

latex

---

clarification:

fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2(j
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;i
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;e);i,e.Req1(i;e);j,i,e.Ack1(j
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;e);i,e.Req1(i;e);j,i,e.Ack1;i
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;e);i,e.Req1(i;e);j,i,e.Ack1;e);i,e.Req2(i
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;e);i,e.Req1(i;e);j,i,e.Ack1;e);i,e.Req2;e);j,i,e.Ack2(j
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;e);i,e.Req1(i;e);j,i,e.Ack1;e);i,e.Req2;e);j,i,e.Ack2;i
fifo+switch(es;C;j,i,e.S1(j;i;e);j,i,e.S2;e);i,e.Req1(i;e);j,i,e.Ack1;e);i,e.Req2;e);j,i,e.Ack2;e))
== (i:C, j:C.
== (x:es-E(es), y:es-E(es).
== (S2(j;i;x)
== ( S1(j;i;y)
== ( ((es-causle(es;x;y)
== ( (( (req:{e:es-E(es)| S2(j;i;e)} 
== ( (( (ack:{e:es-E(es)| Ack2(j;i;e)} 
== ( (( ((Req2(j;req) & es-causle(es;x;req) & es-causle(es;req;ack) & es-causle(es;ack;y))))
== ( & (es-causle(es;y;x)
== ( & ( (req:{e:es-E(es)| S1(j;i;e)} 
== ( & ( (ack:{e:es-E(es)| Ack1(j;i;e)} 
== ( & ( ((Req1(j;req)
== ( & ( (& es-causle(es;y;req)
== ( & ( (& es-causle(es;req;ack)
== ( & ( (& es-causle(es;ack;x))))))
== & (i:C, j:C.
== & ((e:{e:es-E(es)| Ack1(j;i;e)} , e':{e:es-E(es)| Ack1(j;i;e)} .
== & (((es-causle(es;e';e))  es-causl(es; e; e'))
== & (& (e:{e:es-E(es)| Ack2(j;i;e)} , e':{e:es-E(es)| Ack2(j;i;e)} .
== & (& ((es-causle(es;e';e))  es-causl(es; e; e')))
== & (i:C, j:C.
== & ((e:{e:es-E(es)| S1(j;i;e) & Req1(j;e)} , e':{e:es-E(es)| S1(j;i;e) & Req1(j;e)} .
== & (((es-causle(es;e';e))  es-causl(es; e; e'))
== & (& (e:{e:es-E(es)| S2(j;i;e) & Req2(j;e)} , e':{e:es-E(es)| S2(j;i;e) & Req2(j;e)} .
== & (& ((es-causle(es;e';e))  es-causl(es; e; e')))
== & (i:C, j:C.
== & ((e:{e:es-E(es)| S1(j;i;e) & Req1(j;e)} , e':{e:es-E(es)| S1(j;i;e) & Req1(j;e)} .
== & ((es-causl(es; e; e')
== & (( (a:{e:es-E(es)| Ack1(j;i;e)} . (es-causl(es; e; a) & es-causl(es; a; e'))))
== & (& (e:{e:es-E(es)| S2(j;i;e) & Req2(j;e)} , e':{e:es-E(es)| S2(j;i;e) & Req2(j;e)} .
== & (& (es-causl(es; e; e')
== & (& ( (a:{e:es-E(es)| Ack2(j;i;e)} . (es-causl(es; e; a) & es-causl(es; a; e'))))) 

latex

Definitions	A, e c e', x:A. B(x), P  Q, x:A. B(x), {x:A| B(x)} , E, P & Q, (e < e')
FDL editor aliases	fifo+switch